We first present encodings of a simple form of guarded choice and guarded replication. 
Then we use such encodings to encode Minsky machines.


  

  
\subsection{Guarded Choice}  
We extend the \ahopi syntax with a simple form of guarded choice to
choose between different behaviors. 
 Assume,
 for instance, that $a_i$ should trigger $P_i$, for $i\in\{1,2\}$.
We write this as $a_1.P_1 +
 a_2.P_2$, and we write the choice of the behavior $P_i$ as
 $\choice{a_i}$. We then have,  for each $i$, the reduction $(a_1.P_1 +
 a_2.P_2) \parallel \choice{a_i} \pired P_i$. \iflong{We encode these new operators as follows.

\begin{align*}
	\encp{a_1.P_1 + a_2.P_2}{\cho} &= \overline{a_1}\angp{\encp{P_1}{\cho}} \parallel  \overline{a_2}\angp{\encp{P_2}{\cho}}\\
	\encp{\choice{a_1}}{\cho} &= a_{2}(x_{2}).a_1(x_1).x_1\\
	\encp{\choice{a_2}}{\cho} &= a_{1}(x_{1}).a_2(x_2).x_2
\end{align*}
}{We encode $a_1.P_1 +
 a_2.P_2$ as 
\begin{equation*}  
\encp{a_1.P_1 + a_2.P_2}{\cho} = \overline{a_1}\angp{\encp{P_1}{\cho}} \parallel  \overline{a_2}\angp{\encp{P_2}{\cho}}  
%a_1(X_1).\cdots.a_n(X_n).X_1 \parallel a_1(X).\cdots.a_n(Y).Y  
\end{equation*}
the choice
$\encp{\choice{a_1}}{\cho}$ 
as $ a_{2}(x_{2}).a_1(x_1).x_1$, and the choice
$\encp{\choice{a_2}}{\cho}$ 
as $ a_{1}(x_{1}).a_2(x_2).x_2$.}
The translation is an homomorphism on the other operators.   
This way, $\encp{\choice{a_i}}{\cho}$ for $i \in \{1,2\}$ is a process that 
 consumes both $P_i$'s  and spawns the one chosen.
This encoding is correct as long as all guards used in the choices are
  different and  there is at most one message at a guard, 
$\choice{a_1}$ or $\choice{a_2}$ in the previous example, enabled at any given time. 
The encoding introduces an extra communication for every guarded choice.  

With a slight abuse of notation, in what follows
we shall use disjoint sums 
inside \hocore processes without explicitely referring to 
the encoding $\encp{\cdot}{\cho}$.


  
\subsection{Input-guarded Replication}  
% \finish{DS: below, as far as i can see, it is the standard encoding of 
%   replication in HOpi, with restrictin omitted. Is this all, or is 
%   there something  else that i am missing? (otherwise,  it is not very 
%   surprising, and should not be emphasized in introduction and 
%   elsewhere, probably) I guess the fact that the 
%   replications encoded is ``guarded'' is important? }   
We follow the standard encoding of replication in higher-order process
calculi, adapting it to input-guarded replication so as to make sure
that diverging behaviors are not introduced.  As there is no
restriction in \ahopi, the encoding is not compositional and
replications cannot be nested.

%is only correct if the replications may only be triggered once, that is if they are not replicated themselves. A conservative approximation is to require that they are in evaluation context (i.e. in top level parallel compositions).
%\finish{IL: What do you mean here Alan? What's the problem if they are under a prefix? Maybe there are problems if they are nested.} \finish{AS: Is it better?}


\begin{mydefi}
\label{defin:grepl}  
Assume a fresh name $c$. The encoding of \emph{input-guarded replication} is  as follows:  
%$$  
%\encp{!a(z).P}{\inrep} = a(z).(Q_c \parallel P) \parallel \msend{c}{a(z).(Q_c \parallel P)}  
%$$   
\[
\encp{!a(z).P}{\inrep} = a(z).(c(x).(x \parallel \outC{c}\langle x \rangle \parallel P)) 
\parallel \msend{c}{a(z).(c(x).(x \parallel \outC{c}\langle x \rangle \parallel P))}   
\]
where %$Q_c = c(x) .(x \parallel \overline{c}\langle x \rangle)$, 
$P$ contains no replications (nested replications are forbidden),
and $\encp{\cdot}{\inrep}$ is an homomorphism on the  
other process constructs in \ahopi.  
\end{mydefi}





\iflong{%We show that the encoding preserves termination. 
It is worth noticing that after the input on $a$, 
a copy of $P$ is only released after a synchronization on $c$.
More precisely, we have the following correctness statement.
We use $Q \nrightarrow$ to denote that there is no $Q'$ such
 that $Q \pired Q'$, both in \ahopi\ and for Minsky Machines.  

\begin{mylem}[Correctness of $\encp{\cdot}{\inrep}$]  
\label{l:corr-repl}
Let $P$ be a \ahopi process with non-nested input-guarded replications.   
\begin{itemize}  
\item If $\encp{P}{\inrep}  \pired Q$ then $\exists P'$ such that $ P \pired P'$ and  
either $\encp{P'}{\inrep} = Q$ or $Q \pired \encp{P'}{\inrep}$.  
\item If $P \pired P'$ then either $\encp{P}{\inrep} \pired \encp{P'}{\inrep}$ or  
$\encp{P}{\inrep} \pired\pired \encp{P'}{\inrep}$.  
\item $\encp{P}{\inrep} \nrightarrow$ iff $P \nrightarrow$.  
\end{itemize}  
\end{mylem}  

\begin{proof}  
By induction on the transitions.
%By induction on the length of the inference $\xrightarrow{~\alpha~}$.
\end{proof}}{This encoding preserves termination.}  



With a slight abuse of notation, in what follows
we shall use input-guarded replications 
inside \hocore processes without explicitely referring to 
the encoding $\encp{\cdot}{\inrep}$.


\subsection{Minsky machines}\label{subsec:mm2hopi}
We present  an  encoding of Minsky 
machines 
(see Section \ref{ss:expr-approaches})
%\citep{Minsky67} 
into \ahopi. The encoding shows that \ahopi 
is Turing complete and, as the encoding preserves termination, 
it also shows that termination in \ahopi\ is undecidable. 
The only form of non-determinism in the encoding is due to 
possible unfoldings of (the encoding of) recursive definitions after
they have been used; otherwise, at any step, in the encoding any
process  has at most one reduction. 

We first show how to count and test for zero in \ahopi; then, 
we present the encoding of a \mma into \ahopi, denoted as $\encp{\cdot}{\mms}$
(see Table \ref{encod-sum}).
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
 
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
% Encoding for wide margins (one column); next, the version for two columns
\iflong{
\begin{figure}  
\centering  
{\small  
	%\begin{tabular}{|l|}   
	\begin{tabular}{l}   
	       %\hline \\  
		\(   
\begin{array}{lll}   
\multicolumn{3}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mms}& \hspace{-0.2cm} = & \hspace{-0.2cm} !p_i.(\choice{inc_j} \parallel ack.\overline{p_{i+1}}) \\  
\encp{(i: \mathtt{DECJ}(r_j,k))}{\mms}& \hspace{-0.2cm} = & \hspace{-0.2cm}!p_i.(\choice{dec_j} \parallel  ack.(z_j.\overline{p_{k}} + n_{j}. \overline{p_{i+1}} ) \\   
\end{array}   
\) \\  
\(  
\begin{array}{lll} \\  
\multicolumn{2}{l}{\mathrm{\textsc{Registers}}~r_j}\\  
%\encp{r_j = 0}{\mms} & = & (inc_j.(\overline{r^{\mathsf{S}}_j}\angp{\encn{0}{j}}\parallel \overline{ack}) ~+~  
%dec_j.(\regzero{j}  \parallel \rz{j} \parallel \overline{ack})) \parallel \mathsf{REG}_j \\  
%\encp{r_j = m}{\mms} & = & (inc_j.(\overline{r^{\mathsf{S}}_j} \angp{\encn{m}{j}} \parallel  \overline{ack}) ~+~ 
%dec_j.(\encn{m-1}{j}\parallel \overline{ack})) \parallel  \mathsf{REG}_j \\  
\encp{r_j = 0}{\mms} & = & (inc_j.\overline{r^{\mathsf{S}}_j}\angp{\encn{0}{j}} ~+~  
dec_j.(\regzero{j}  \parallel \rz{j} )) \parallel \mathsf{REG}_j \\  
\encp{r_j = m}{\mms} & = & (inc_j.\overline{r^{\mathsf{S}}_j} \angp{\encn{m}{j}}  ~+~ 
dec_j.\encn{m-1}{j}) \parallel  \mathsf{REG}_j \\  
\end{array}  
\) \\   
\quad where: \\ % the shorthand notation $\encn{k}$ is defined as follows: \\  
\quad   
\(  
\begin{array}{lll}  
\mathsf{REG}_j & = & !r^0_j.( \overline{ack} \parallel inc_j.\regsucc{j}{\encn{0}{j}} ~+~   
dec_j.(\regzero{j}  \parallel \rz{j} )) \parallel \\  
& & !r^{\mathsf{S}}_j(Y).(   \overline{ack} \parallel 
inc_j. \regsucc{j}{\regsucc{j}{Y} \parallel  \rnz{j}} ~+~ dec_j.Y ) \\   
\end{array}  
\) \\   
\quad \quad \quad \(  
\encn{k}{j}=\left\{  
\begin{array}{ll}  
 \regzero{j}  \parallel \rnz{j} & \textrm{if } k= 0 \\  
 \regsucc{j}{\encn{k-1}{j}} \parallel   \rnz{j} & \textrm{if } k> 0 .  
\end{array}\right.  
\) \\ %\\  
%\hline  
\end{tabular}  
\caption{Encoding of Minsky machines into \ahopi}  
\label{encod-sum}  
}  
\end{figure}  
}{
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
\begin{table}  
\centering  
{\small  
	%\begin{tabular}{|l|}   
	\begin{tabular}{l}   
	       %\hline \\  
		\(   
\begin{array}{lll}   
\multicolumn{3}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mms}& \hspace{-0.2cm} = & \hspace{-0.2cm} !p_i.(\choice{inc_j} \parallel ack.\overline{p_{i+1}}) \\  
\encp{(i: \mathtt{DECJ}(r_j,k))}{\mms}& \hspace{-0.2cm} = & \hspace{-0.2cm}!p_i.(\choice{dec_j} \parallel  ack.(z_j.\overline{p_{k}} + n_{j}. \overline{p_{i+1}} ) \\   
\end{array}   
\) \\  
\(  
\begin{array}{lll} \\  
\multicolumn{3}{l}{\mathrm{\textsc{Registers}}~r_j}\\  
%\encp{r_j = 0}{\mms} & = & inc_j.(\overline{r^{\mathsf{S}}_j}\angp{\encn{1}{j}}\parallel \overline{ack}  \parallel \mathsf{REG}) ~+~ \\  
%& & dec_j.(\encn{0}{j} \parallel \overline{ack} \parallel \mathsf{REG}) \\  
%\encp{r_j = m}{\mms} & = & inc_j.(\overline{r^{\mathsf{S}}_j} \angp{\encn{m}{j}} \parallel  \overline{ack}  \parallel \mathsf{REG}) ~+~ \\
%& & dec_j.(\encn{m-1}{j}\parallel \overline{ack} \parallel  \mathsf{REG}) \\  
\encp{r_j = 0}{\mms} & = & (inc_j.(\overline{r^{\mathsf{S}}_j}\angp{\encn{1}{j}}\parallel \overline{ack}) ~+~  \\
& & ~~ dec_j.(\encn{0}{j} \parallel \overline{ack})) \parallel \mathsf{REG}_j \\  
\encp{r_j = m}{\mms} & = & (inc_j.(\overline{r^{\mathsf{S}}_j} \angp{\encn{m}{j}} \parallel  \overline{ack}) ~+~ \\
& & ~~ dec_j.(\encn{m-1}{j}\parallel \overline{ack})) \parallel  \mathsf{REG}_j \\  
\end{array}  
\) \\   
\quad where: \\ % the shorthand notation $\encn{k}$ is defined as follows: \\  
\quad   
\(  
\begin{array}{lll}  
\mathsf{REG}_j & = & !r^0_j.(inc_j.(\regsucc{j}{\encn{1}{j}} \parallel \overline{ack}) ~+~ \\   
& & ~~~~ \quad dec_j.(\encn{0}{j} \parallel \overline{ack})) \parallel \\  
& & !r^{\mathsf{S}}_j(Y).(   
inc_j. (\regsucc{j}{\regsucc{j}{Y} \parallel  \rnz{j}}  \parallel \overline{ack}) ~+~\\   
& &  ~~~ \quad \quad \quad dec_j.(Y \parallel  \overline{ack}) ) \\   
\end{array}  
\) \\   
\quad \quad \quad \(  
\encn{k}{j}=\left\{  
\begin{array}{ll}  
 \regzero{j}  \parallel \rz{j} & \textrm{if } k= 0 \\  
 \regsucc{j}{\encn{k-1}{j}} \parallel   \rnz{j} & \textrm{if } k> 0 .  
\end{array}\right.  
\) \\ %\\  
%\hline  
\end{tabular}  
\caption{Encoding of Minsky machines}  
\label{encod-sum}  
}  
\end{table}  
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
  
  
\paragraph{Counting in \ahopi.} The cornerstone of our encoding is the definition of counters that may be tested for zero. Numbers are represented as nested higher-order processes:   
the encoding of a number $k+1$ in register $j$, denoted $\encn{k+1}{j}$,  
is the parallel composition of two processes: $\regsucc{j}{\encn{k}{j}}$ (the successor of $\encn{k}{j}$) and a flag $\rnz{j}$.  
%indicating the number is not zero. 
The encoding of zero comprises such a flag, as well as the message $\regzero{j}$. 
% and a flag $\rz{j}$ indicating it is zero.  
As an example,
$\encn{2}{j}$ is  
%The encoding of $2$ is thus 
$\regsucc{j}{\regsucc{j}{\regzero{j} \parallel \rnz{j}} \parallel \rnz{j}} \parallel \rnz{j}$.

\paragraph{Registers.}
Registers are counters that may be incremented and decremented. They consist of two parts: their current state and two mutually recursive processes used to generate a new state after an increment or decrement of the register. The state depends on whether the current value of the register is zero or not, but in both cases it consists of a choice between an increment and a decrement. In case of an increment, a message on $\regsuccname{j}$ is sent containing the current register value, for instance $m$. This message is then received by the recursive definition of $\regsuccname{j}$ that creates a new state with value $m+1$, ready for further increment or decrement. In case of a decrement, the behavior depends on the current value, as specified in the reduction relation in Table \ref{fig:mmdef}. If the current value is zero, then it stays at zero, recreating the state corresponding to zero for further operations using the message on $\regzeroname{j}$, and it spawns a flag $\rz{j}$ indicating that a decrement on a zero-valued register has occurred. If the current value $m$ is strictly greater than zero, then the process $\encn{m-1}{j}$ is spawned. If $m$ was equal to $1$, this puts the state of the register to zero (using a message on $\regzeroname{j}$). Otherwise, it keeps the message in a non-zero state, with value $m-1$, using a message on $\regsuccname{j}$. In both cases a flag $\rnz{j}$ is spawned to indicate that the register was not equal to zero before the decrement. When an increment or decrement has been processed, that is when the new current state has been created, an acknowledgment is sent to proceed with the execution of the next instruction.

\paragraph{Instructions.}  
The encoding of instructions goes hand in hand with the encoding of registers.  
Each instruction $(i:I_i)$ is a replicated process guarded by $p_i$, which represents the program counter when $p=i$.   
Once $p_i$ is consumed, the instruction is active and an interaction with a register occurs. In case of an increment instruction, the corresponding choice is sent to the relevant register and, upon reception of the acknowledgment, the next instruction is spawned. In case of a decrement, the corresponding choice is sent to the register, then an acknowledgment is received followed by a choice depending on whether the register was zero, resulting in a jump to the specified instruction, or the spawning of the next instruction otherwise.  
  
The encoding of a configuration of a \mma thus requires a finite number of fresh names (linear on $n$, the number of instructions).  
\begin{mydefi}\label{encod-conf}  
Let $N$ be a \mma with registers $r_0 = m_0$, $r_1=m_1$ and instructions  
$(1:I_1), \ldots, (n:I_n)$.  
Suppose fresh, pairwise different names $\regzeroname{j}$, $\regsuccname{j}$, $p_1, \ldots, p_n$, $inc_j$, $dec_j$, $ack$ (for $j \in \{0,1\}$).  
Given the encodings in Table \ref{encod-sum},   
a configuration $(i, m_0, m_1)$ of $N$ is encoded as  
\begin{equation*}  
%\encp{(i, m_0, m_1) }{\mms} =  
\overline{p_i} \parallel \encp{r_0 = m_0}{\mms} \parallel \encp{r_1 = m_1}{\mms} \parallel   \prod^{n}_{i=1} \encp{(i:I_i)}{\mms} \,.
\end{equation*}  
\end{mydefi}  
  
  
\paragraph{Correctness of the Encoding.}  
  

In \ahopi, we write  $ \longrightarrow^* $  for the reflexive and transitive
closure of $\longrightarrow $,
and $P \divpired$ if $P$ has an infinite sequence of reductions.
Similarly, in Minsky machines 
 $\minskred^*$ is the reflexive and transitive closure of $\minskred$,
% and $\notminskred$ when no reduction is possible. We also write 
and
$N \divminskred$ means that $N$ has an infinite sequence of reductions.


% We now show that our encoding simulates Minsky machines deterministically and faithfully (i.e. it preserves divergence).  
  
%\finish{DS: below is it up to $\equiv$? } 
\begin{mylem} \label{l:corr_minsky}
Let $N$ be a \mma. We have:  
\begin{enumerate}  
	\item $N \minskred^{*} N'$ iff $\encp{N}{\mms} \pired^{*} \encp{N'}{\mms}$;  
	\item if $\encp{N}{\mms} \pired^{*} P_1$ and $\encp{N}{\mms} \pired^{*} P_2$, then there exists $N'$ such that $P_1 \pired^* \encp{N'}{\mms}$ and $P_2 \pired^* \encp{N'}{\mms}$;  
	\item $N \divminskred$ iff $\encp{N}{\mms} \divpired$.  
\end{enumerate}  
\end{mylem}  
%\iflong{ %The long description of the rule starts here  
%\begin{proof}
%Moved to an appendix.
%\end{proof}
%}{ % Short explanation of the proof  
%\begin{proof}%[Proof (Sketch)]  

The proof of Lemma \ref{l:corr_minsky} %, which is detailed in Appendix \ref{s:app_minsky}, 
relies on two properties. 
The first one, given by Lemma \ref{l:sound},
ensures that for every computation of the Minsky machine
the encoding can perform a 
finite, 
non-empty sequence of reductions that correspond to the one made by the machine.
Using Lemma \ref{l:corr-repl}, the second property (Lemma \ref{l:complete}) ensures that 
% \iflong{\as{What is the corresponding lemma in the appendix?}}{} 
if the process encoding a Minsky machine
has a reduction then 
(i) the machine also has a reduction, and  (ii) the encoding has a finite sequence of reductions
that correspond to the result of the reduction of the Minsky machine. 
%The only non-determinism is due to the unfolding of recursive definitions, 
%which, s
%Since recursion is guarded,  adds at most a finite number of reductions for each step of the Minsky machine, thus divergence is never introduced.
%\as{Discussion about termination is missing.}
%it will eventually lead to a state that corresponds to the subsequente state of the Minsky machine. 
%  We show that there is a tight relationship between the execution of 
%  $N$ and an invariant structure of its encoding, the only 
%  non-determinism coming from choosing when to unfold 
%recursive processes 
%after their use. One can then show that every finite 
%  computation of the \mma  is mimicked by a finite computation of the 
%  encoding. 
%\iflong{Full details can be found in Appendix .}{}
%\end{proof}
 

\input{lics-proof_minsky}


The results above guarantee that \ahopi is Turing complete, and since
the encoding preserves termination, it entails the following
corollary.


\begin{mycoro}  
Termination in \ahopi is undecidable.  
\end{mycoro}  
  
  
  
  
  
  
